Nuprl Definition : es_realizer_ind
11,40
es_realizer_ind(
x1
;
es_realizer_ind(
none
;
es_realizer_ind(
left
,
right
,
rec1
,
rec2
.
plus
(
left
;
right
;
rec1
;
rec2
);
es_realizer_ind(
loc
,
T
,
x
,
v
.
init
(
loc
;
T
;
x
;
v
);
es_realizer_ind(
loc
,
T
,
x
,
L
.
frame
(
loc
;
T
;
x
;
L
);
es_realizer_ind(
lnk
,
tag
,
L
.
sframe
(
lnk
;
tag
;
L
);
es_realizer_ind(
loc
,
ds
,
knd
,
T
,
x
,
f
.
effect
(
loc
;
ds
;
knd
;
T
;
x
;
f
);
es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.
sends
(
ds
;
knd
;
T
;
l
;
dt
;
g
);
es_realizer_ind(
loc
,
ds
,
a
,
p
,
P
.
pre
(
loc
;
ds
;
a
;
p
;
P
);
es_realizer_ind(
loc
,
k
,
L
.
aframe
(
loc
;
k
;
L
);
es_realizer_ind(
loc
,
k
,
L
.
bframe
(
loc
;
k
;
L
);
es_realizer_ind(
loc
,
x
,
L
.
rframe
(
loc
;
x
;
L
))
== case
x1
==
of inl(
x
) =>
none
== o
| inr(
x
) => case
x
== o| inr(
x
) =>
of inl(
x
) =>
plus
(
x
.1
== o| inr(
x
) => of inl(
x
) =>
plus
;
x
.2
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind((
x
.1);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
none
;
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
left
,
right
,
rec1
,
rec2
.
plus
(
left
;
right
;
rec1
;
rec2
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
loc
,
T
,
x
,
v
.
init
(
loc
;
T
;
x
;
v
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
loc
,
T
,
x
,
L
.
frame
(
loc
;
T
;
x
;
L
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
lnk
,
tag
,
L
.
sframe
(
lnk
;
tag
;
L
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
loc
,
ds
,
knd
,
T
,
x
,
f
.
effect
(
loc
;
ds
;
knd
;
T
;
x
;
f
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.
sends
(
ds
;
knd
;
T
;
l
;
dt
;
g
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
loc
,
ds
,
a
,
p
,
P
.
pre
(
loc
;
ds
;
a
;
p
;
P
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
loc
,
k
,
L
.
aframe
(
loc
;
k
;
L
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
loc
,
k
,
L
.
bframe
(
loc
;
k
;
L
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
loc
,
x
,
L
.
rframe
(
loc
;
x
;
L
))
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind((
x
.2);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
none
;
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
left
,
right
,
rec1
,
rec2
.
plus
(
left
;
right
;
rec1
;
rec2
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
loc
,
T
,
x
,
v
.
init
(
loc
;
T
;
x
;
v
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
loc
,
T
,
x
,
L
.
frame
(
loc
;
T
;
x
;
L
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
lnk
,
tag
,
L
.
sframe
(
lnk
;
tag
;
L
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
loc
,
ds
,
knd
,
T
,
x
,
f
.
effect
(
loc
;
ds
;
knd
;
T
;
x
;
f
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
ds
,
knd
,
T
,
l
,
dt
,
g
.
sends
(
ds
;
knd
;
T
;
l
;
dt
;
g
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
loc
,
ds
,
a
,
p
,
P
.
pre
(
loc
;
ds
;
a
;
p
;
P
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
loc
,
k
,
L
.
aframe
(
loc
;
k
;
L
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
loc
,
k
,
L
.
bframe
(
loc
;
k
;
L
);
== o| inr(
x
) => of inl(
x
) =>
plus
;es_realizer_ind(
loc
,
x
,
L
.
rframe
(
loc
;
x
;
L
)))
== o| inr(
x
) => o
| inr(
x
) => case
x
== o| inr(
x
) => o| inr(
x
) =>
of inl(
x
) =>
init
(
x
.1;(
x
.2).1;(
x
.2.2).1;
x
.2.2.2)
== o| inr(
x
) => o| inr(
x
) => o
| inr(
x
) => case
x
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
of inl(
x
) =>
frame
(
x
.1;(
x
.2).1;(
x
.2.2).1;
x
.2.2.2)
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o
| inr(
x
) => case
x
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
of inl(
x
) =>
sframe
(
x
.1;(
x
.2).1;
x
.2.2)
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o
| inr(
x
) => case
x
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
of inl(
x
) =>
effect
(
x
.1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
effect
;(
x
.2).1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
effect
;(
x
.2.2).1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
effect
;(
x
.2.2.2).1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
effect
;(
x
.2.2.2.2).1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
effect
;
x
.2.2.2.2.2)
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o
| inr(
x
) => case
x
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
of inl(
x
) =>
sends
(
x
.1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
sends
;(
x
.2).1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
sends
;(
x
.2.2).1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
sends
;(
x
.2.2.2).1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
sends
;(
x
.2.2.2.2).1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
sends
;
x
.2.2.2.2.2)
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o
| inr(
x
) => case
x
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
of inl(
x
) =>
pre
(
x
.1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
pre
;(
x
.2).1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
pre
;(
x
.2.2).1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
pre
;(
x
.2.2.2).1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
pre
;
x
.2.2.2.2)
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o
| inr(
x
) => case
x
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
of inl(
x
) =>
aframe
(
x
.1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
aframe
;(
x
.2).1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
aframe
;
x
.2.2)
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o
| inr(
x
) => case
x
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
of inl(
x
) =>
bframe
(
x
.1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
bframe
;(
x
.2).1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => of inl(
x
) =>
bframe
;
x
.2.2)
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o
| inr(
x
) =>
rframe
(
x
.1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
rframe
;(
x
.2).1
== o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) => o| inr(
x
) =>
rframe
;
x
.2.2)
(recursive)
latex
Definitions
Y
,
x
.
A
(
x
)
,
f
(
a
)
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
t
.1
,
t
.2
FDL editor aliases
es_realizer_ind
origin
x.A(x)x.A(x)